{-
 -  Separ, Type/Base.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

{-# LANGUAGE ExistentialQuantification #-}

-- Module Base
-- Basic types and definitions
-- Substitute and SubstitueM (M for monadic version)
-- Context, MulticontextMonad and operation for them
-- uniGetVars (variable scanner) and related occurCheck
-- important type classes (mainly a hack to handle cyclic 
--     dependencies between modules)
--

module Type.Base where

import Prelude hiding (log,id)

import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.List as List
import qualified System.IO.Unsafe
import Control.Monad
import qualified Control.Monad.State as CMSt 

import qualified GHC.Read as GR
import qualified Text.Read as TR
import qualified Text.ParserCombinators.ReadP as RP
import qualified Text.ParserCombinators.ReadPrec as TP

import qualified Data.IntSet as RefSet
import qualified Data.IntMap as RefMap
import qualified Data.IntMap as EqMap

import Type.ClsType

import qualified Type.Parser.ParType as PPar
import qualified Type.Parser.AbsType as PAbs
import qualified Type.Parser.ErrM    as PErr

-------------------------------------------
-- types and basic manipulation
-------------------------------------------

-- to store unhandled formulae there is a store for them
-- ids help with recognizing where some formula came from
-- type of identifiers of equations and id -> equation map
type EqId = Int               
type EqMap a = EqMap.IntMap a
-- type of references i.e. variables
type RefType = Int            
-- type for sets of references
-- used e.g. by occur check
type RefSet = RefSet.IntSet
type RefMap a = RefMap.IntMap a -- type for map holding values of variables
type TagType = Int            -- type of tag

-- type for instantiation/skolemization data
-- True = skolem, False = inst, RefType holds the var in question
data FInfo = FInfo [(Bool,RefType)] deriving Show
(+++) :: FInfo -> FInfo -> FInfo
(FInfo a) +++ (FInfo b) = FInfo $ a ++ b

-- type for main terms
data Type = Cls ClsType -- class
	| Ref RefType       -- reference
	| Lca Type Type     -- lowest common ancestor
	| Gcd Type Type     -- greatest common descendant

	-- lambda expression
	-- Lam direction argument result
	-- False means result <-- argument 
	-- True  means argument --> result
	| Lam Bool Type Type  
						  
	-- variable introduction (quantifier)
	-- Var variable (loBound,hiBound) guard type
	-- loBound and hiBound with respect to 'leq' ordering
	-- i.e. for no constraints use typeNothing and typeThing respectively
	-- guard are formulae for type which can express additional constraints
	| Var RefType (Type,Type) Formulae Type 

	-- application
	-- App direction function argument
	-- like in lambda, 
	-- False means function(argument) 
	-- True  means (argument)function
	| App Bool Type Type

	-- Add Property
	-- PSet type propertyName propertyValue
	| PSet Type String Type

	-- Get Property
	-- PGet type propertyName
	| PGet Type String
	deriving (Eq,Ord)

typeThing :: Type
typeThing = Cls clsThing     -- top type
typeNothing :: Type
typeNothing = Cls clsNothing -- bottom type
typeNothingThing :: Type
typeNothingThing = Cls clsNothingThing -- Nothing[* = Thing]
typeThingNothing :: Type
typeThingNothing = Cls clsThingNothing -- Thing[* = Nothing]

typeIsThing :: Type -> Bool
typeIsThing (Cls c) | clsIsThing c = True
typeIsThing (Cls _) | otherwise    = False
typeIsThing _ = False

typeIsNothing :: Type -> Bool
typeIsNothing (Cls c) | clsIsNothing c = True
typeIsNothing (Cls _) | otherwise    = False
typeIsNothing _ = False

typeIsNothingThing :: Type -> Bool
typeIsNothingThing (Cls c) | clsIsNothingThing c = True
typeIsNothingThing (Cls _) | otherwise    = False
typeIsNothingThing _ = False

typeIsThingNothing :: Type -> Bool
typeIsThingNothing (Cls c) | clsIsThingNothing c = True
typeIsThingNothing (Cls _) | otherwise    = False
typeIsThingNothing _ = False


-- pSet constructor
pSet :: Type -> String -> Type -> Type
pSet t _ v | typeIsThing v = t
pSet t s v | otherwise     = PSet t s v

-- type for formulae (plural because of 'And' constructor)
data Formulae = TT | FF -- truth and falsehood
	
	-- logical conjunction of formulae
	-- there is no disjunction, this is handled by
	-- multiple states/contexts
	| And [Formulae]

	-- equality assertion
	| Eq Type Type      

	-- inequality assertion
	-- if Bool is true then variable <: Type means variable = Type
	-- rest behaves normally, it is used mainly for constraint 
	-- in application (traditional <: would make variables too lose)
	| Leq Bool Type Type 

	-- variable introduction in formulae
	-- Qua quantificationType variableReference bounds guard formulae
	-- in quantificationType field
	--     True denotes universal quantification, False -- existential
	-- bounds and guard are just like in Type, 
	| Qua Bool RefType (Type,Type) Formulae Formulae
		deriving (Eq,Ord)

-- logic and with some simplification
-- mainly used for adding a new term to the (And ls) list
fand :: Formulae -> Formulae -> Formulae
fand TT y = y
fand x TT = x
fand FF _ = FF
fand _ FF = FF
fand (And xs) (And ys) = And $ xs ++ ys
fand (And xs) y = And $ y:xs
fand x (And ys) = And $ x:ys
fand x y = And [x,y]

-- used in quantify in Type.Quantifiers to handle cases like
-- (var x. Thing) or (forall x. TT) to keep it just in Thing/TT form
-- TODO this should check for variables inside if they are used or not
typeIsConstant :: Type -> Bool
typeIsConstant (Cls _) = True
typeIsConstant (Lca a b) = and $ map typeIsConstant [a,b]
typeIsConstant (Gcd a b) = and $ map typeIsConstant [a,b]
typeIsConstant (Lam _ a r) = and $ map typeIsConstant [a,r]
typeIsConstant (App _ f x) = and $ map typeIsConstant [f,x]
typeIsConstant (PSet t _ v) = and $ map typeIsConstant [t,v]
typeIsConstant (PGet t _) = typeIsConstant t
typeIsConstant (Ref _) = False
typeIsConstant (Var _ _ _ _) = False

-- and same for formulae
formulaeIsConstant :: Formulae -> Bool
formulaeIsConstant TT = True
formulaeIsConstant FF = True
formulaeIsConstant (And ls) = and $ map formulaeIsConstant ls
formulaeIsConstant (Eq a b) = and $ map typeIsConstant [a,b]
formulaeIsConstant (Leq _ a b) = and $ map typeIsConstant [a,b]
formulaeIsConstant (Qua _ _ _ _ _) = False

-- printing of Type and Formulae

showParen' True  exp = showString "{" . exp . showString "}"
showParen' False exp = exp

showBound d (hi, lo) | typeIsNothing hi && typeIsThing lo = showString ""
showBound d (hi, lo) | typeIsNothing hi = showString " : " . showsPrec 0 lo
showBound d (hi, lo) | otherwise = 
	showString " : " . showsPrec 0 lo . showString " -- " . showsPrec 0 hi

showForms d TT    = showString ""
showForms d forms = showString " ; " . showsPrec 0 forms

instance Show Type where
	showsPrec d (Ref r) = showParen' (d > 10) $ showsPrec d r
	showsPrec d (Cls c) = showParen' (d > 10) $ showsPrec d c
	showsPrec d (Lca a b) = showParen' (d > 4) $ showsPrec 5 a . showString " `sup` " . showsPrec 4 b
	showsPrec d (Gcd a b) = showParen' (d > 5) $ showsPrec 6 a . showString " `inf` " . showsPrec 5 b
	showsPrec d (Lam False a r) = showParen' (d > 2) $ showsPrec 2 r . showString " <-- " . showsPrec 4 a
	showsPrec d (Lam True a r) = showParen' (d > 3) $ showsPrec 4 a . showString " --> " . showsPrec 3 r
	showsPrec d (App False f x) = showParen' (d > 7) $ showsPrec 7 f . showString "(" . showsPrec 0 x . showString ")"
	showsPrec d (App True f x) = showParen' (d > 6) $ showString "(" . showsPrec 0 x . showString ")" . showsPrec 6 f
	showsPrec d (Var r b f t) = showString "{ " . showsPrec 0 r . showBound 0 b .
			showForms 0 f . showString " | " . showsPrec 0 t . showString " }"
	showsPrec d (PSet t n v) = showParen' (d > 8) $ showsPrec 8 t . 
			showString "[" . showString n .	showString " : " . showsPrec 0 v . showString "]"
	showsPrec d (PGet t n) = showParen' (d > 8) $ showsPrec 8 t . showString "[" . showString n . showString "]"

instance Show Formulae where
	showsPrec d (TT) = showString "TT"
	showsPrec d (FF) = showString "FF"
	showsPrec d (And []) = showString "TT"
	showsPrec d (And [x]) = showsPrec d x
	showsPrec d (And (x:xs)) = showsPrec d x . showString ", " . showsPrec d (And xs)
	showsPrec d (Eq a b) = showsPrec 0 a . showString " = " . showsPrec 0 b
	showsPrec d (Leq _ a b) = showsPrec 0 a . showString " <: " . showsPrec 0 b
	showsPrec d (Qua True var bound forms expb) = showString "{ forall " . showsPrec 0 var . 
		showBound 0 bound . showForms 0 forms . showString " | " . showsPrec 0 expb . showString "}" 
	showsPrec d (Qua False var bound forms expb) = showString "{ exists " . showsPrec 0 var .
		showBound 0 bound . showForms 0 forms . showString " | " . showsPrec 0 expb . showString "}" 

-- parsing Type and Formulae
type ParState = CMSt.State (RefType, Map.Map String RefType) -- uniq, env

fromDecl :: PAbs.Decl -> ParState (String, (Type, Type))
fromDecl (PAbs.DeclV (PAbs.LoIdent (_,name))) = do 
	return (name, (typeNothing, typeThing))
fromDecl (PAbs.DeclL (PAbs.LoIdent (_,name)) hiBound) = do
	hiBound' <- fromExp hiBound
	return (name, (typeNothing, hiBound'))
fromDecl (PAbs.DeclB (PAbs.LoIdent (_,name)) hiBound loBound) = do
	hiBound' <- fromExp hiBound
	loBound' <- fromExp loBound
	return (name, (loBound', hiBound'))

fromExpBoolT :: PAbs.ExpBoolT -> ParState Formulae
fromExpBoolT (PAbs.EBTN) = return TT
fromExpBoolT (PAbs.EBTJ []) =  return TT
fromExpBoolT (PAbs.EBTJ (PAbs.BTT:xs)) =  fromExpBoolT (PAbs.EBTJ xs)
fromExpBoolT (PAbs.EBTJ ls) =  liftM And $ mapM fromExpBool ls

fromDeclList :: PAbs.DeclList -> (RefType -> (Type,Type) -> Formulae -> a -> a) -> ParState a -> ParState a
fromDeclList (PAbs.DL [] guard) constructor obj = obj
fromDeclList (PAbs.DL (x:xs) guard) constructor obj =
	fromDeclList' x (PAbs.EBTJ []) constructor $ 
		fromDeclList (PAbs.DL xs guard) constructor obj
fromDeclList' decl guard constructor obj = do
	(name, bound) <- fromDecl decl
	(uniq, env) <- CMSt.get
	CMSt.put (uniq + 1, Map.insert name uniq env)
	guard' <- fromExpBoolT guard
	obj' <- obj
	(uniq', _) <- CMSt.get
	CMSt.put (uniq', env)
	return $ constructor uniq bound guard' obj'

fromClass :: PAbs.Class -> ClsType
fromClass (PAbs.UPI (PAbs.UpIdent (_, name))) = read name
fromClass (PAbs.UPL ls) = clsInf $ map fromClass ls

fromExp :: PAbs.Exp -> ParState Type
fromExp (PAbs.Cls cls) = do return $ Cls $ fromClass cls
fromExp (PAbs.Ref (PAbs.LoIdent (_, name))) = do 
	(uniq, env) <- CMSt.get
	case Map.lookup name env of
		Just ref -> return $ Ref ref
		Nothing  -> fail $ "Unknown name: " ++ name
fromExp (PAbs.Var [] exp) = do fromExp exp
fromExp (PAbs.Var (d:ds) exp) = do
	fromDeclList d Var $ fromExp (PAbs.Var ds exp)
fromExp (PAbs.PSF exp (PAbs.LoIdent (_, property)) value) = undefined -- TODO
fromExp (PAbs.PST exp (PAbs.LoIdent (_, property)) value) = do
	exp' <- fromExp exp
	value' <- fromExp value
	return $ pSet exp' property value'
fromExp (PAbs.PGF exp (PAbs.LoIdent (_, property))) = undefined -- TODO
fromExp (PAbs.PGT exp (PAbs.LoIdent (_, property))) = do
	exp' <- fromExp exp
	return $ PGet exp' property
fromExp (PAbs.AppF func arg) = do
	func' <- fromExp func
	arg' <- fromExp arg
	return $ App False func' arg'
fromExp (PAbs.AppT arg func) = do
	func' <- fromExp func
	arg' <- fromExp arg
	return $ App True func' arg'
fromExp (PAbs.Sup a b) = do
	a' <- fromExp a 
	b' <- fromExp b
	return $ Lca a' b'
fromExp (PAbs.Inf a b) = do
	a' <- fromExp a
	b' <- fromExp b
	return $ Gcd a' b'
fromExp (PAbs.LamF r a) = do
	a' <- fromExp a
	r' <- fromExp r
	return $ Lam False a' r'
fromExp (PAbs.LamT a r) = do
	a' <- fromExp a
	r' <- fromExp r
	return $ Lam True a' r'

fromExpBool (PAbs.BTT) = do return TT
fromExpBool (PAbs.BFF) = do return FF
fromExpBool (PAbs.BEQ a b) = do
	a' <- fromExp a
	b' <- fromExp b
	return $ Eq a' b'
fromExpBool (PAbs.BLEQ a b) = do
	a' <- fromExp a
	b' <- fromExp b
	return $ Leq False a' b'
fromExpBool (PAbs.BQT [] expB) = do fromExpBool expB
fromExpBool (PAbs.BQT (d:ds) expB) = do
	fromDeclList d (Qua True) $ fromExpBool (PAbs.BQT ds expB)
fromExpBool (PAbs.BQF [] expB) = do fromExpBool expB
fromExpBool (PAbs.BQF (d:ds) expB) = do
	fromDeclList d (Qua False) $ fromExpBool (PAbs.BQF ds expB)

instance Read Type where
	readPrec = do
		str <- TP.lift $ RP.manyTill RP.get RP.eof
		case PPar.pExp $ PPar.myLexer str of
			PErr.Bad _   -> TP.pfail
			PErr.Ok tree -> return $ CMSt.evalState (fromExp tree) (1, Map.empty)
	readListPrec = TR.readListPrecDefault

instance Read Formulae where
	readPrec = do
		str <- TP.lift $ RP.manyTill RP.get RP.eof
		case PPar.pExpBool $ PPar.myLexer str of
			PErr.Bad _   -> TP.pfail
			PErr.Ok tree ->	return $ CMSt.evalState (fromExpBool tree) (1, Map.empty)
	readListPrec = TR.readListPrecDefault

-- class for objects on which substitute can act
-- basically Types and Formulae
-- beware only single substitution works now (because of Var and Qua)
-- TODO fix it
class Substitutable a where
	substy :: (RefType -> Maybe Type) -> a -> a

-- utility function for generating substitutions of a single variable
-- subRef variableToSubstitute valueToSubstitute referenceInQuestion
subRef :: RefType -> Type -> RefType -> Maybe Type
subRef r t x = if r == x then Just t else Nothing

instance Substitutable Type where
	substy _ (Cls s) = (Cls s)
	substy p (Ref rt) = case p rt of
		Just t  ->  t
		Nothing -> (Ref rt)
	substy p (Lca a b) = (Lca (substy p a) (substy p b))
	substy p (Gcd a b) = (Gcd (substy p a) (substy p b))
	substy p (Lam b t1 t2) = (Lam b (substy p t1) (substy p t2))
	substy p t@(Var rt (a,b) f t1) = 
		-- there is no check whether a <: t <: b or f(t) here
		-- but should it be? probably it should be where substy is called
		case p rt of
		Just _ -> t -- TODO beware now only single substitution works
		Nothing -> (Var rt (substy p a, substy p b) (substy p f) (substy p t1))
	substy p (App b t1 t2) = (App b (substy p t1) (substy p t2))
	substy p (PSet t n v) = (PSet (substy p t) n (substy p v))
	substy p (PGet t n) = (PGet (substy p t) n)

instance Substitutable Formulae where
	substy _ TT = TT
	substy _ FF = FF
	substy p (And ls) = (And $ List.map (substy p) ls)
	substy p (Eq a b) = (Eq (substy p a) (substy p b))
	substy p (Leq e a b) = (Leq e (substy p a) (substy p b))
	substy p f@(Qua q v (a,b) f1 f2) = 
		-- analogous problem
		-- no check whether a <: t <: b or f1(t)
		case p v of
		Just _ -> f -- TODO beware now only single substitution works
		Nothing -> (Qua q v (substy p a, substy p b) (substy p f1) (substy p f2))
	
-------------------------------------------------
-- CONTEXT and context manipulation
-------------------------------------------------

-- Data of variable (represented by a reference of type RefType)
data VarData = VarData
	{ bounds   :: (Type,Type) -- bounds, e.g. (typeNothing,typeThing)
	, formulae :: Formulae    -- a guard, formulae from constructor
	
	-- some variables have its own quantifier
	-- (if introduced from (Var...) or (Qua...)),
	-- but some have not (e.g. if instantiated x would be 
	-- turned to a lambda expression x1 --> x2, then where
	-- x1 and x2 should be quantified?)
	-- parent denotes variable at quantifier of which this
	-- variable should be forallized (parent r == r means
	-- that var has its own quantifier)
	, parent   :: RefType     

	-- value of variable
	-- if x = Ref  x -- it is instantiated var
	-- if x = Ref -x -- it is skolemized var
	-- otherwise it is just bound
	, value    :: Type

	-- instantiation/skolemization time tag (when var was unquantified)
	, timeTag  :: TagType     

	-- references of vars that should be forallized with this var
	-- if y = parent x then x \in children y, 
	-- especially z \in children z if z has its own quantifier
	, children :: [RefType]
	} deriving Show

-- Context
-- holds everything you want to know about current computation
data Context = CTX 
	{ uniqRef_ :: RefType 	  -- generator of unique references
	, log_ :: [String]        -- for debugging purposes

	-- main map holding data of vars
	-- the most important record of context
	, varMap_ :: RefMap VarData 

	, uniqEqId_ :: EqId       -- generator of ids for EqMap
	, uniqTag_ :: TagType     -- generator for inst/skol
	
	-- non-empty stack of maps of formulae (generally eqs and leqs)
	-- it is a stack to separate some sub-computations like
	-- normalizing guard of skolemized variable
	, eqMap_ :: [EqMap Formulae]

	-- this one is set to true if some var has been bound
	-- used for checks if another round of normalization should be run
	, bindMark_ :: Bool
	} deriving Show

-- empty context for starters (e.g. function testMM)
ctxEmpty :: Context
ctxEmpty = CTX { uniqRef_ = clsN*1000, log_ = [], varMap_ = RefMap.empty, -- TODO is 1000 per class enough?
				 uniqEqId_ = 1, uniqTag_ = 1, eqMap_ = [EqMap.empty],
				 bindMark_ = False }
-- and some appropriate checks
ctxIsEmpty :: Context -> Bool
ctxIsEmpty c = and [RefMap.null $ varMap_ c, and $ map EqMap.null $ eqMap_ c]

----------------------------------
-- context functions
----------------------------------

-- I believe names are self-explanatory
-- BTW all the names start with ctx prefix and 
-- this is really annoying!
-- Haskell module system should help with this,
-- however, recursive dependencies do not help
-- (actually not in this case, but still)

-- b     -- bounds
-- c     -- ctx
-- ch    -- child/children
-- d     -- data
-- f     -- formulae
-- i     -- id
-- p     -- reference of parent
-- r     -- main reference
-- v     -- value

ctxIsRefFree :: RefType -> Context -> Bool
ctxIsRefFree r c = RefMap.notMember r $ varMap_ c

ctxLog :: String -> Context -> Context
ctxLog string c = c {log_ = string : (log_ c)}
ctxGetLog :: Context -> [String]
ctxGetLog c = log_ c

-- separate stored formulae
ctxPushEqMap :: Context -> Context
ctxPushEqMap c = c {eqMap_ = EqMap.empty : eqMap_ c}
ctxPopEqMap :: Context -> Context
ctxPopEqMap c = case eqMap_ c of
	[] -> error $ "ctxPopEqMap panic! empty eqMaps stack!"
	_:[] -> error $ "ctxPopEqMap panic! too smal eqMaps stack!"
	x:y:xs -> let y' = EqMap.unionWithKey 
			(\k _ _ -> error $ "ctxPopEqMap repeated eqId: " ++ show k) x y 
		in c {eqMap_ = y':xs}
-- store some formula (mainly Eqs or Leqs)
ctxPushEq :: Formulae -> Context -> (Context,EqId)
ctxPushEq f c = 
	let ru = uniqEqId_ c in
	case eqMap_ c of
		[] -> error $ "ctxPushEq panic! empty eqMaps stack!"
		x:xs -> let x' = EqMap.insert ru f x in
			(c {uniqEqId_ = ru + 1, eqMap_ = x':xs},ru)
-- restore formula stored under id returned by pushEq
ctxPopEq :: EqId -> Context -> (Context,Maybe Formulae)
ctxPopEq i c = case eqMap_ c of
	[] -> error $ "ctxPopEq panic! empty eqMaps stack!"
	x:xs -> (c {eqMap_ = (EqMap.delete i x):xs}, EqMap.lookup i x)
-- peek
ctxGetEq :: EqId -> Context -> Maybe Formulae
ctxGetEq i c = case eqMap_ c of
	[] -> error $ "ctxGetEq panic! empty eqMaps stack!"
	x:_ -> EqMap.lookup i x
-- set
ctxSetEq :: EqId -> Formulae -> Context -> Context
ctxSetEq i f c = case eqMap_ c of
	[] -> error $ "ctxSetEq panic! empty eqMaps stack!"
	x:xs -> c {eqMap_ = (EqMap.insert i f x):xs}

-- get unique ref
ctxUniqRef :: Context -> (Context,RefType)
ctxUniqRef c = let ru = uniqRef_ c in
	(c {uniqRef_ = ru + 1}, ru)
-- get some tag, separated form refs
ctxUniqTag :: Context -> (Context,TagType)
ctxUniqTag c = let ru = uniqTag_ c in
	(c {uniqTag_ = ru + 1}, ru)

ctxGetVarData :: RefType -> Context -> Maybe VarData
ctxGetVarData r c = RefMap.lookup r (varMap_ c)
ctxGetVarDataUnsafe :: RefType -> Context -> VarData
ctxGetVarDataUnsafe r c = case ctxGetVarData r c of
	Nothing -> error $ "unknown reference (" ++ show r ++ ")"
	Just d -> d
ctxSetVarData :: RefType -> VarData -> Context -> Context
ctxSetVarData r d c = let ru' = max (uniqRef_ c) (r+1) in
	c {varMap_ = RefMap.insert r d $ varMap_ c, uniqRef_ = ru'}
ctxDelVarData :: RefType -> Context -> Context
ctxDelVarData r c = 
	if RefMap.notMember r $ varMap_ c then 
		error $ "tried to delete unknown reference (" ++ show r ++ ")"
	else c {varMap_ = RefMap.delete r $ varMap_ c}

-- get function which can be used with substitute or substituteM
ctxGetSubstyFun :: Context -> RefType -> Maybe Type
ctxGetSubstyFun c r = do
	d <- ctxGetVarData r c
	return $ value d

ctxGetVarBounds :: RefType -> Context -> (Type,Type)
ctxGetVarBounds r c = bounds $ ctxGetVarDataUnsafe r c
ctxSetVarBounds :: RefType -> (Type,Type) -> Context -> Context
ctxSetVarBounds r b c = 
	let d = (ctxGetVarDataUnsafe r c) {bounds = b} in
	ctxSetVarData r d c

ctxGetVarFormulae :: RefType -> Context -> Formulae
ctxGetVarFormulae r c = formulae $ ctxGetVarDataUnsafe r c
ctxSetVarFormulae :: RefType -> Formulae -> Context -> Context
ctxSetVarFormulae r f c = 
	let d = (ctxGetVarDataUnsafe r c) {formulae = f} in
	ctxSetVarData r d c

ctxGetVarParent :: RefType -> Context -> RefType
ctxGetVarParent r c = parent $ ctxGetVarDataUnsafe r c
ctxSetVarParent :: RefType -> RefType -> Context -> Context
ctxSetVarParent r p c = 
	let d = (ctxGetVarDataUnsafe r c) {parent = p} in
	ctxSetVarData r d c
-- WARNING just value, not 'last' value of a chain of references
ctxGetVarValue :: RefType -> Context -> Type
ctxGetVarValue r c = value $ ctxGetVarDataUnsafe r c
ctxSetVarValue :: RefType -> Type -> Context -> Context
ctxSetVarValue r v c = 
	let d  = ctxGetVarDataUnsafe r c in
	let c' = ctxDelVarChild (parent d) r c in
	let d' = d {value = v} in
	ctxSetVarData r d' c'

-- set BindM to False
ctxClearBindM :: Context -> Context
ctxClearBindM c = c {bindMark_ = False}
ctxGetBindM :: Context -> Bool
ctxGetBindM c = bindMark_ c
ctxSetBindM :: Bool -> Context -> Context
ctxSetBindM mark c = c {bindMark_ = mark}

ctxGetVarTimeTag :: RefType -> Context -> TagType
ctxGetVarTimeTag r c = timeTag $ ctxGetVarDataUnsafe r c

ctxGetVarChildren :: RefType -> Context -> [RefType]
ctxGetVarChildren r c = children $ ctxGetVarDataUnsafe r c
ctxAddVarChild :: RefType -> RefType -> Context -> Context
ctxAddVarChild p r c = 
	let d = ctxGetVarDataUnsafe p c in
	let d' = d {children = r:(children d)} in
	ctxSetVarData p d' c
ctxDelVarChild :: RefType -> RefType -> Context -> Context
ctxDelVarChild p r c = 
	let d = ctxGetVarDataUnsafe p c in
	if notElem r $ children d then 
		error $ "tried to delete unknown child (" ++ show r ++ ")"
	else let d' = d {children = List.delete r $ children d} in
	ctxSetVarData p d' c

-- puts variable into a context
ctxNewVar :: Bool -> RefType -> (Type,Type) -> Formulae -> RefType ->
	Context -> Context
ctxNewVar skol r b f p c = 
	let (c',tag) = ctxUniqTag c in
	let c'' = ctxSetVarData r 
		(VarData {bounds = b, formulae = f, parent = p, 
		value = (Ref $ if skol then -r else r), 
		timeTag = tag, children = []}) c'
	in ctxAddVarChild p r c''
ctxNewVarInst :: RefType -> (Type,Type) -> Formulae -> RefType ->
	Context -> Context
ctxNewVarInst = ctxNewVar False
ctxNewVarSkolem :: RefType -> (Type,Type) -> Formulae -> RefType ->
	Context -> Context
ctxNewVarSkolem = ctxNewVar True

-- turn any free var to inst var
ctxMakeVarInst :: RefType -> Context -> Context
ctxMakeVarInst r c = 
	let d = ctxGetVarDataUnsafe r c in
	case value d of
		(Ref s) -> if s == r || s == -r then
				let d' = d {value = Ref r} in
				ctxSetVarData r d' c
			else error "tried to MkInst bound var"
		_ -> error "tried to MkInst bound var"
-- turn any free var to skolem
ctxMakeVarSkolem :: RefType -> Context -> Context
ctxMakeVarSkolem r c = 
	let d = ctxGetVarDataUnsafe r c in
	case value d of
		(Ref s) -> if s == r || s == -r then
				let d' = d {value = Ref $ -r} in
				ctxSetVarData r d' c
			else error "tried to MkSkolem bound var"
		_ -> error "tried to MkSkolem bound var"

-- is bound, inst or skolem
ctxIsVar :: RefType -> Context -> Bool
ctxIsVar r c = case ctxGetVarData r c of
	Nothing -> False
	Just _ -> True
-- is free = is inst or skolem
ctxIsVarFree :: RefType -> Context -> Bool
ctxIsVarFree r c = case ctxGetVarValue r c of
	(Ref s) -> s == r || s == -r
	_ -> False
ctxIsVarSkolem :: RefType -> Context -> Bool
ctxIsVarSkolem r c = case ctxGetVarValue r c of
	(Ref s) -> s == -r
	_ -> False
ctxIsVarInst :: RefType -> Context -> Bool
ctxIsVarInst r c = case ctxGetVarValue r c of
	(Ref s) -> s == r
	_ -> False

-- removes variable from context and all its children recursively
-- appropriate parents/children records are removed too
ctxDelVar :: RefType -> Context -> Context
ctxDelVar r c = 
	let p = ctxGetVarParent r c in
	let c' = ctxDelVarChild p r c in
	let ch = ctxGetVarChildren r c' in
	let c'' = foldr ctxDelVar c' ch in
	ctxDelVarData r c''


-------------------------------------------------
-- Multi-state Monad
-------------------------------------------------
--
-- the core of state/context handling
-- I messed with similar thing in Java for almost a year,
-- it was horrible. Here this is just nice and clean.
-- In short Haskell rox ^^
--  
-- TODO
-- for now it is list of possible states/contexts 
-- but it should be a priority queue sorted for probability
-- this is not hard to code, but leave it that way for now
--
-- moreover there should be check for inserting very same values
-- i.e. [Unknown,Unknown,Unknown] should be just [Unknown]
-- (important performance issues)
--

newtype MM a = MM (Context -> [(Context,a)])
runMM :: forall t. MM t -> Context -> [(Context, t)]
runMM (MM g) c = g c
testMM :: forall b. (Show b) => MM b -> [b]
testMM m = List.map f $ runMM m ctxEmpty where
	f (c,a) = if ctxIsEmpty c then a 
		else error $ "result: " ++ show a ++ "\n with non-empty context: " ++ show c

instance Functor (MM) where
	fmap f (MM g) = (MM $ \c -> List.map (\(d,x) -> (d,f x)) (g c))
instance Monad (MM) where
	return x = MM (\c -> [(c,x)])
	fail "" = MM $ \_ -> []
	fail s = 
-- !!! WARNING UNSAFE PERFORM IO !!!
		let !_ = System.IO.Unsafe.unsafePerformIO 
			(putStrLn $ "    " ++ s) in
		-- if you would want to throw errors, do it here
		MM $ \_ -> [] -- error s
	(MM g) >>= f = (MM (\c ->
		let m (d,x) = runMM (f x) d in
		List.concatMap m (g c))) -- TODO some hashing and uniq here?

instance MonadPlus (MM) where
	mzero = MM $ \_ -> []
	mplus (MM f) (MM g) = MM (\c -> f c ++ g c)

-- version of if for use with (>>=)
-- e.g. isVarFree r >>= choice (liftM snd $ getVarBounds r) (getVarValue r)
choice :: t -> t -> Bool -> t
choice a b t = if t then a else b
-- something a'la "try G with F" meaning
-- try to compute G and if G fails (state list is empty) then F
inCase :: MM a -> MM a -> MM a
inCase (MM f) (MM g) = MM $ \c -> let r = g c in
	if null r then f c else r
-- because of too many repeats
-- here is a function which will (hopefully) deal with it
unique :: Ord a => [a] -> [a]
unique ls = Set.toList $ Set.fromList $ ls
uniqueM :: Ord a => MM a -> MM a
uniqueM (MM f) = let swap (a,b) = (b,a) in MM $ \c -> 
	map swap $ Map.toList $ Map.fromList $ map swap $ f c

-- substitue with resolution of bound references
-- beware only single substitution works now (because of Var and Qua)
-- TODO fix it
class SubstitutableM a where
	substyM :: (RefType -> Maybe Type) -> a -> MM a
instance SubstitutableM Type where
	substyM m (Ref r) = do
		free <- isVar r >>= choice (isVarFree r) (return True)
		if free then case m r of
				Just t  -> return t
				Nothing -> return (Ref r)
		-- hate this if/do Haskell syntax issue 
		-- (it is going to be corrected in 6.14,
		-- but I use 6.12 version now...)
			else do 
				v <- getVarValue r 
				v' <- substyM m v
				updateVarValue r v'
				return v'
	substyM _ (Cls s) = return (Cls s)
	substyM p (Lca a b) = liftM2 Lca (substyM p a) (substyM p b)
	substyM p (Gcd a b) = liftM2 Gcd (substyM p a) (substyM p b)
	substyM p (Lam b t1 t2) = liftM2 (Lam b) (substyM p t1) (substyM p t2)
	substyM p t@(Var rt (a,b) f t1) = -- no check whether a <: t <: b or f(t)
		case p rt of
		Just _ -> return t -- TODO beware only single substy works
		Nothing -> do 
			a' <- substyM p a
			b' <- substyM p b
			f' <- substyM p f
			t1' <- substyM p t1
			return (Var rt (a', b') (f') (t1'))
	substyM p (App b t1 t2) = liftM2 (App b) (substyM p t1) (substyM p t2)
	substyM p (PSet t n v) = do
		t' <- substyM p t
		v' <- substyM p v
		return $ pSet t' n v'
	substyM p (PGet t n) = liftM (flip PGet n) (substyM p t)
instance SubstitutableM Formulae where
	substyM _ TT = return TT
	substyM _ FF = return FF
	substyM p (And ls) = do
		ls' <- mapM (substyM p) ls
		return (And ls')
	substyM p (Eq a b) = liftM2 Eq (substyM p a) (substyM p b)
	substyM p (Leq e a b) = liftM2 (Leq e) (substyM p a) (substyM p b)
	substyM p f@(Qua q v (a,b) f1 f2) = 
		-- no check whether a <: t <: b or f1(t)
		case p v of
		Just _ -> return f -- TODO beware, now only single substy works
		Nothing -> do
			a' <- substyM p a
			b' <- substyM p b
			f1' <- substyM p f1
			f2' <- substyM p f2
			return (Qua q v (a', b') (f1') (f2'))

-- get and set monad's context
getCtx :: MM Context
getCtx = MM $ \c -> [(c,c)]
setCtx :: Context -> MM ()
setCtx c = MM $ \_ -> [(c,())]

-- some utilities
-- !!! WARNING UNSAFE PERFORM IO !!!
log :: String -> MM ()
log s = MM $ \c -> [(ctxLog s c,())]
getLog :: MM [String]
getLog = MM $ \c -> [(c,ctxGetLog c)]
{-# NOINLINE showLog #-}
showLog :: MM ()
showLog = MM $ \c -> [(c,
	System.IO.Unsafe.unsafePerformIO (putStrLn $ head $ ctxGetLog c))]
{-# NOINLINE prn_ #-}
prn_ :: String -> a -> a
prn_ s x = let !_ = System.IO.Unsafe.unsafePerformIO (putStrLn s) in x
{-# NOINLINE prn #-}
prn :: String -> MM ()
prn s = prn_ s $ MM $ \c -> [(c,())]
-- this one is really use full, but beware of lazy evaluation
-- on the other hand, the probability that 
-- monad won't enforce correct order (of prints) is small
{-# NOINLINE shw #-}
shw :: Show s => s -> MM ()
shw s = prn $ show s
-- END OF WARNING

-- get unique reference, tag or whatever
uniqRef :: MM RefType
uniqRef = MM $ \c -> [ctxUniqRef c]
uniqTag :: MM TagType
uniqTag = MM $ \c -> [ctxUniqTag c]

getVarData :: RefType -> MM VarData
getVarData r = MM $ \c -> case ctxGetVarData r c of
	Nothing -> prn_ ("unknown reference (" ++ show r ++ ")") []
	Just d -> [(c,d)]
setVarData :: RefType -> VarData -> MM ()
setVarData r d = MM $ \c -> [(ctxSetVarData r d c,())]
delVarData :: RefType -> MM ()
delVarData r = MM $ \c -> [(ctxDelVarData r c,())]

isRefFree :: RefType -> MM Bool
isRefFree r = MM $ \c -> [(c,ctxIsRefFree r c)]
testRefFree :: RefType -> MM (Maybe RefType)
testRefFree r = MM $ \c ->
	--if ctxIsRefFree r c then [(c,Nothing)]
	--else 
	-- TODO hack: assume ref is never free, error by occur check with
    -- Ref x = ... Var x () ...
		let (c',r') = ctxUniqRef c in [(c',Just r')]

pushEqMap :: MM ()
pushEqMap = MM $ \c -> [(ctxPushEqMap c,())]
popEqMap :: MM ()
popEqMap = MM $ \c -> [(ctxPopEqMap c,())]
pushEq :: Formulae -> MM EqId
pushEq f = MM $ \c -> [ctxPushEq f c]
popEq :: EqId -> MM Formulae
popEq i = MM $ \c -> case ctxPopEq i c of
	(_ ,Nothing) -> error $ "unknown eq id (" ++ show i ++ ")"
	(c',Just f) -> [(c',f)]
getEq :: EqId -> MM Formulae
getEq i = MM $ \c -> case ctxGetEq i c of
	Nothing -> error $ "unknown eq id (" ++ show i ++ ")"
	Just f -> [(c,f)]
setEq :: EqId -> Formulae -> MM ()
setEq i f = MM $ \c -> [(ctxSetEq i f c,())]

getVarBounds :: RefType -> MM (Type,Type)
getVarBounds r = liftM bounds $ getVarData r
setVarBounds :: RefType -> (Type,Type) -> MM ()
setVarBounds r b = do
	d <- getVarData r
	setVarData r $ d {bounds = b}
getVarFormulae :: RefType -> MM Formulae
getVarFormulae r = liftM formulae $ getVarData r
setVarFormulae :: RefType -> Formulae -> MM ()
setVarFormulae r f = do
	d <- getVarData r
	setVarData r $ d {formulae = f}
getVarParent :: RefType -> MM RefType
getVarParent r = liftM parent $ getVarData r
setVarParent :: RefType -> RefType -> MM ()
setVarParent r p = do
	d <- getVarData r
	setVarData r $ d {parent = p}

-- gets just what is in varData
getVarValue_ :: RefType -> MM Type
getVarValue_ r = liftM value $ getVarData r
-- resolves chain references and updates context
-- sadly var which is bound to some other skolem
-- (and other similar cases) will have one more call here
-- (I think it is cheaper that ifs and (Ref .) matching)
getVarValue :: RefType -> MM Type
getVarValue r = do
	v <- getVarValue_ r
	case v of
		(Ref s) -> if s == r || s == -r then return (Ref r) else do
			u <- getVarValue s
			updateVarValue r u -- this is not proper bind, just a rebind
			return u
		_ -> return v
setVarValue :: RefType -> Type -> MM ()
setVarValue r v = do
	d <- getVarData r
	let t = case value d of {(Ref s) -> s == r; _ -> False}
	unless t $ error $ "tried bind Var" ++ show (r,value d) ++") to " ++ show v
	setVarData r $ d {value = v}
	setBindM True
-- used as rebind, without BindM and checks
updateVarValue :: RefType -> Type -> MM ()
updateVarValue r v = do
	d <- getVarData r
	setVarData r $ d {value = v}
clearBindM :: MM ()
clearBindM = MM $ \c -> [(ctxClearBindM c,())]
getBindM :: MM Bool
getBindM = MM $ \c -> [(c,ctxGetBindM c)]
setBindM :: Bool -> MM ()
setBindM b = MM $ \c -> [(ctxSetBindM b c,())]
getVarTimeTag :: RefType -> MM TagType
getVarTimeTag r = liftM timeTag $ getVarData r
-- gets whole list of time tags from x to root parent (head element)
getVarTimeTags :: RefType -> MM [TagType]
getVarTimeTags r0 = getVarTimeTags' r0 [] where
	getVarTimeTags' r a = do
		t <- getVarTimeTag r
		p <- getVarParent r
		if p == r then return (t:a) else getVarTimeTags' p (t:a)
getVarChildren :: RefType -> MM [RefType]
getVarChildren r = liftM children $ getVarData r
addVarChild :: RefType -> RefType -> MM ()
addVarChild p r = do
	--shw ("addC",p,r)
	d <- getVarData p
	setVarData p $ d {children = r:(children d)}
delVarChild :: RefType -> RefType -> MM ()
delVarChild p r = do
	--shw ("delC",p,r)
	d <- getVarData p
	if notElem r $ children d then 
		error $ "tried to delete unknown child (" ++ show r ++ ")"
		else setVarData p $ d {children = List.delete r $ children d}
	
newVar :: Bool -> RefType -> (Type,Type) -> Formulae -> RefType -> MM ()
newVar q r b f p = do
	t <- uniqTag
	refFree <- isRefFree r
	unless refFree $ error $ "newVar using taken ref tag"
	setVarData r $ VarData {bounds = b, formulae = f, parent = p, 
		value = (Ref $ if q then -r else r), timeTag = t, children = []}
	addVarChild p r
newVarInst :: RefType -> (Type,Type) -> Formulae -> RefType -> MM ()
newVarInst = newVar False
newVarSkolem :: RefType -> (Type,Type) -> Formulae -> RefType -> MM ()
newVarSkolem = newVar True

makeVarInst :: RefType -> MM ()
makeVarInst r = do
	d <- getVarData r
	case value d of
		(Ref s) -> if s == r || s == -r then
				setVarData r $ d {value = Ref r}
			else error "tried to reinstantiate bound var"
		_ -> error "tried to reinstantiate f bound var"
makeVarSkolem :: RefType -> MM ()
makeVarSkolem r = do
	d <- getVarData r
	case value d of
		(Ref s) -> if s == r || s == -r then
				setVarData r $ d {value = Ref (-r)}
			else error "tried to reskolemize bound var"
		_ -> error "tried to reskolemize bound var"

-- is var in context (bind, skolem or inst)
isVar :: RefType -> MM Bool
isVar r = MM $ \c -> case ctxGetVarData r c of
	Nothing -> [(c,False)]
	Just _ -> [(c,True)]
-- is var inst or skolem
isVarFree :: RefType -> MM Bool
isVarFree r = do
	v <- getVarValue_ r
	case v of
		(Ref s) -> do
			return $ s == r || s == -r
		_ -> return False
isVarSkolem :: RefType -> MM Bool
isVarSkolem r = do
	v <- getVarValue_ r
	case v of {(Ref s) -> return $ s == -r;	_ -> return False}
isVarInst :: RefType -> MM Bool
isVarInst r = do
	v <- getVarValue_ r
	case v of {(Ref s) -> return $ s == r; _ -> return False}

delVar :: RefType -> MM ()
delVar r = do
	p <- getVarParent r
	delVarChild p r
	ch <- getVarChildren r
	mapM_ delVar ch
	delVarData r


-------------------------------------------
-- UniGetVars
-- gets all variables and also occur checks
-------------------------------------------

class UniGetVars a where	
	uniGetVars :: a -> RefSet -> MM RefSet
	occurCheck :: a -> MM RefSet
	occurCheck a = uniGetVars a RefSet.empty
data UniGetVarsType = forall a. UniGetVars a => UGV a
instance UniGetVars UniGetVarsType where
	uniGetVars (UGV t) = uniGetVars t
instance UniGetVars a => UniGetVars [a] where
	uniGetVars [] rs = return rs
	uniGetVars (x:xs) rs = uniGetVars x rs >>= (uniGetVars xs)
instance UniGetVars Type where
	uniGetVars (Ref r) rs = isVar r >>= choice (do
		free <- isVarFree r
		case (free,RefSet.member r rs) of -- occur check
			(False,False) -> getVarValue r >>= 
				(flip uniGetVars $ RefSet.insert r rs) >>=
				(return . (RefSet.delete r))
			(False,True) -> do
				v <- getVarValue r
				fail $ "occur check failed for (Ref " ++
					show r ++ ") = " ++ show v
			(True,False) -> do
				f <- getVarFormulae r
				(no,th) <- getVarBounds r
				uniGetVars [UGV f,UGV no,UGV th] (RefSet.insert r rs)
			(True,True) -> return rs)
		(return $ RefSet.insert r rs)
	uniGetVars (Cls _)      rs = return rs
	uniGetVars (Lca a b)    rs = uniGetVars [a,b] rs
	uniGetVars (Gcd a b)    rs = uniGetVars [a,b] rs
	uniGetVars (Lam _ a r)  rs = uniGetVars [a,r] rs
	uniGetVars (App _ f x)  rs = uniGetVars [f,x] rs
	uniGetVars (Var r (no,th) f t) rs = 
		(uniGetVars [UGV [no,th,t],UGV f] rs) >>= 
			(return . (RefSet.delete r))
	uniGetVars (PSet t _ v) rs = uniGetVars [t,v] rs
	uniGetVars (PGet t _)   rs = uniGetVars  t    rs
instance UniGetVars Formulae where
	uniGetVars  TT         rs = return rs
	uniGetVars  FF         rs = return rs
	uniGetVars (And fs)    rs = uniGetVars  fs   rs
	uniGetVars (Eq a b)    rs = uniGetVars [a,b] rs
	uniGetVars (Leq _ a b) rs = uniGetVars [a,b] rs
	uniGetVars (Qua _ r (no,th) f1 f2) rs = 
		(uniGetVars [UGV [no,th],UGV [f1,f2]] rs) >>= 
			(return . (RefSet.delete r))


-- some additional utility functions abstracted from
-- handling loops of equation normalization, bounds optimization, etc.
-- k denotes continuation
eqLoopK :: (EqId -> Type -> Type -> MM b -> MM b)
        -> (EqId -> Bool -> Type -> Type -> MM b -> MM b) -> MM b -> MM b
eqLoopK fe fl k = do
	clearBindM
	(eqs,leqs) <- eqGetEqs
	eqFold fe eqs $ eqFold2 fl leqs $ 
		getBindM >>= (choice (eqLoopK fe fl k) k)

eqGetEqs :: MM ([(EqId, Type, Type)],[(EqId, Bool, Type, Type)])
eqGetEqs = do
	ctx <- getCtx
	let (oldEqMap,eqMapTail) = case eqMap_ ctx of
		[] -> error $ "eqGetEqs panic! eqMap stack empty!"
		m:ms -> (m,ms)
	let (lists,newEqMap) = EqMap.mapAccumWithKey f ([],[]) $ oldEqMap
		where
			f    (eqs,leqs) k (Eq a b) = (((k,a,b):eqs,leqs),TT)
			f    (eqs,leqs) k (Leq e a b) = ((eqs,(k,e,a,b):leqs),TT)
			f ys            k (And xs) = List.foldl g (ys,TT) xs where
				g (a,b) x = let (a',b') = f a k x in (a', fand b b')
			f ys            _ g = (ys,g)
	setCtx $ ctx {eqMap_ = newEqMap:eqMapTail}
	return lists

-- fold for Eqs
eqFold :: (i -> a -> b -> k -> k)
           -> [(i, a, b)] -> k -> k 
eqFold _ [] k = k
eqFold f ((id,a,b):xs) k = f id a b $ eqFold f xs k
-- fold for Leqs
eqFold2 :: (i -> e -> a -> b -> k -> k)
           -> [(i, e, a, b)] -> k -> k 
eqFold2 _ [] k = k
eqFold2 f ((id,e,a,b):xs) k = f id e a b $ eqFold2 f xs k
-- store back in map
eqEqOk :: EqId -> Type -> Type -> MM a -> MM a
eqEqOk id a b k = getEq id >>= (setEq id . (fand (Eq a b))) >>= (const k)
eqLeqOk :: EqId -> Bool -> Type -> Type -> MM a -> MM a
eqLeqOk id e a b k = getEq id >>= (setEq id . (fand (Leq e a b))) >>= (const k)

-----------------------------------------
-- important type-classes 
-----------------------------------------

-- instances defined in Type.Quantifiers
class Quantifiable a where
	quantify :: FInfo -> a -> MM a
	unquantify :: Bool -> a -> MM (a,FInfo)
	{-# SPECIALIZE quantify :: FInfo -> Type -> MM Type #-}
	{-# SPECIALIZE unquantify :: Bool -> Type -> MM (Type,FInfo) #-}
	{-# SPECIALIZE quantify :: FInfo -> Formulae -> MM Formulae #-}
	{-# SPECIALIZE unquantify :: Bool -> Formulae -> MM (Formulae,FInfo) #-}

-- instances defined in Type.Normalize
class Normalizable a where
	normalize :: forall b. a -> MM b -> MM (a,b)
	{-# SPECIALIZE normalize :: Type -> MM b -> MM (Type,b) #-}
	{-# SPECIALIZE normalize :: Formulae -> MM b -> MM (Formulae,b) #-}
	{-# SPECIALIZE normalize :: FInfo -> MM b -> MM (FInfo,b) #-}

data NormalizableType = forall a. Normalizable a => N a

-- instances defined in Type.Satisfiability
class Ensurable a where
	ensure :: a -> MM ()
	{-# SPECIALIZE ensure :: Formulae -> MM () #-}

-- instances defined in Type.Quantifiers
class Lambdable a where
	makeLam :: Bool -> Bool -> a -> MM (a,a,FInfo)
	{-# SPECIALIZE makeLam :: Bool -> Bool -> Type -> MM (Type,Type,FInfo) #-}

-- instances defined in Type.Eval
class Evaluable a where
	eval :: a -> MM a
	{-# SPECIALIZE eval :: Type -> MM Type #-}

-- instnaces defined in Type.Satisiability
class UniLoop a where
	uniLoopK :: MM a -> MM a
 
-- end
